/-
Copyright (c) 2025 Dexin Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dexin Zhang
-/
module

public import Mathlib.GroupTheory.GroupAction.SubMulAction.Closure

/-!
# Semigroup ideals

This file defines (left) semigroup ideals (also called monoid ideals sometimes), which are sets `s`
in a semigroup such that `a * b ∈ s` whenever `b ∈ s`. Note that semigroup ideals are different from
ring ideals (`Ideal` in Mathlib): a ring ideal is a semigroup ideal that is also an additive
submonoid of the ring.

## References

* [Samuel Eilenberg and M. P. Schützenberger, *Rational Sets in Commutative Monoids*][eilenberg1969]
-/

@[expose] public section

open Set Pointwise

/-- A (left) semigroup ideal in a semigroup `M` is a set `s` such that `a * b ∈ s` whenever
`b ∈ s`. -/
@[to_additive /-- A (left) additive semigroup ideal in an additive semigroup `M` is a set `s` such
that `a + b ∈ s` whenever `b ∈ s`. -/]
abbrev SemigroupIdeal (M : Type*) [Mul M] :=
  SubMulAction M M

namespace SemigroupIdeal

variable {M : Type*}

section Mul

variable [Mul M] {s t : Set M} {x : M}

@[to_additive]
protected theorem mul_mem (I : SemigroupIdeal M) (x : M) {y : M} : y ∈ I → x * y ∈ I :=
  SubMulAction.smul_mem I x

/-- The semigroup ideal generated by a set `s`. -/
@[to_additive /-- The additive semigroup ideal generated by a set `s`. -/]
abbrev closure (s : Set M) : SemigroupIdeal M :=
  SubMulAction.closure M s

@[to_additive]
theorem mem_closure : x ∈ closure s ↔ ∀ p : SemigroupIdeal M, s ⊆ p → x ∈ p :=
  SubMulAction.mem_closure

@[to_additive]
theorem subset_closure : s ⊆ closure s :=
  SubMulAction.subset_closure

@[to_additive]
theorem mem_closure_of_mem (hx : x ∈ s) : x ∈ closure s :=
  SubMulAction.mem_closure_of_mem hx

@[to_additive]
theorem closure_le {I} : closure s ≤ I ↔ s ⊆ I :=
  SubMulAction.closure_le

@[to_additive (attr := gcongr)]
theorem closure_mono (h : s ⊆ t) : closure s ≤ closure t :=
  SubMulAction.closure_mono h

end Mul

/-- The semigroup ideal generated by `s` is `s ∪ Set.univ * s`. -/
@[to_additive /-- The additive semigroup ideal generated by `s` is `s ∪ Set.univ + s`. -/]
theorem coe_closure [Semigroup M] {s : Set M} :
    (closure s : Set M) = s ∪ univ * s := by
  let I : SemigroupIdeal M :=
    { carrier := s ∪ univ * s
      smul_mem' x y := by
        rintro (hy | ⟨y, -, z, hz, rfl⟩)
        · exact .inr <| mul_mem_mul (mem_univ _) hy
        · simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz }
  suffices closure s = I by rw [this]; rfl
  refine (closure_le.2 fun x => Or.inl).antisymm fun x hx => hx.elim mem_closure_of_mem ?_
  rintro ⟨y, -, z, hz, rfl⟩
  exact SemigroupIdeal.mul_mem _ _ (mem_closure_of_mem hz)

@[to_additive, inherit_doc coe_closure]
theorem mem_closure' [Semigroup M] {s : Set M} {x : M} :
    x ∈ closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x := by
  rw [← SetLike.mem_coe, coe_closure]
  simp [mem_mul]

attribute [inherit_doc AddSemigroupIdeal.coe_closure] AddSemigroupIdeal.mem_closure'

/-- In a monoid, the semigroup ideal generated by `s` is `Set.univ * s`. -/
@[to_additive /-- In an additive monoid, the semigroup ideal generated by `s` is `Set.univ + s`. -/]
theorem coe_closure' [Monoid M] {s : Set M} :
    (closure s : Set M) = univ * s := by
  rw [coe_closure, union_eq_right]
  exact fun x hx => ⟨1, mem_univ 1, x, hx, by simp⟩

@[to_additive, inherit_doc coe_closure']
theorem mem_closure'' [Monoid M] {s : Set M} {x : M} :
    x ∈ closure s ↔ ∃ y, ∃ z ∈ s, y * z = x := by
  rw [← SetLike.mem_coe, coe_closure']
  simp [mem_mul]

attribute [inherit_doc AddSemigroupIdeal.coe_closure'] AddSemigroupIdeal.mem_closure''

/-- A semigroup ideal is finitely generated if it is generated by a finite set.

This is defeq to `SubMulAction.FG`, but unfolds more nicely. -/
@[to_additive /-- An additive semigroup ideal is finitely generated if it is generated by a finite
set.

This is defeq to `SubAddAction.FG`, but unfolds more nicely. -/]
def FG [Mul M] (I : SemigroupIdeal M) :=
  ∃ (s : Set M), s.Finite ∧ I = closure s

@[to_additive]
theorem fg_iff [Mul M] {I : SemigroupIdeal M} : I.FG ↔ ∃ (s : Finset M), I = closure s :=
  SubMulAction.fg_iff

end SemigroupIdeal
